\begin{tabbing}
$\forall$\=$E$:Type, ${\it eq}$:EqDecider($E$), ${\it prd}$:($E$$\rightarrow$($E$+Unit)), ${\it info}$:($E$$\rightarrow$(Id$\times$Id+(IdLnk$\times$$E$)$\times$Id)),\+
\\[0ex]${\it oax}$:EOrderAxioms($E$; ${\it prd}$; ${\it info}$), $T$:(Id$\rightarrow$Id$\rightarrow$Type), $w$, $a$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$)),
\\[0ex]${\it sax}$:($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ ($\forall$$x$:Id. $w$($x$,$e$) $=$ $a$($x$,pred($e$)) $\in$ $T$(loc($e$),$x$))), $V$:(Knd$\rightarrow$Id$\rightarrow$Type),
\\[0ex]$v$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))).
\-\\[0ex]mk{-}eval($E$;${\it eq}$;${\it prd}$;${\it info}$;${\it oax}$;$T$;$w$;$a$;${\it sax}$;$V$;$v$) $\in$ EventsWithValues
\end{tabbing}